in mcs-dep

mod MCS-EXP is
  inc MCS-CHECK .
  eq Bound = 8 .
  var OCs : Soup{OComp} .
  var P : Pid .
endm

red in MCS-EXP : modelCheck(init6,lofree1) .

search in MCS-EXP : init6 =>* {(depth: 8) OCs} .